ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{e:es-E(es)| 
ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), es:event_system{i:l}, i:Id, e1,e2:{loc(e) = i} ,
e:es-E(es).
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 es-locl(es; e1; e)
 es-le(es; e; e2)
 (es-hist{i:l}(es;e1;e2)
 (=
 (append(es-hist{i:l}(es;e1;es-pred(es; e)); es-hist{i:l}(es;e;e2))
 ( (event-info(ds;da) List)) 

latex

Definitions	x:A. B(x), P  Q, top, es-hist{i:l}(es;e1;e2), t  T, x. t(x), P  Q, A c B, sq_type(T), guard(T), prop{i:l}, P  Q, x(s), es-locl(es; e; e')
Lemmas	map append sq, es-interval wf, es-pred wf, es-locl-iff, es-le wf, es-locl wf, es-E wf, Id wf, es-loc wf, es-valtype wf, fpf-cap wf, Knd wf, Kind-deq wf, es-kind wf, top wf, es-vartype wf, id-deq wf, event system wf, fpf wf, es-le-loc, es-loc-pred, es-interval-partition, map wf, event-info wf, Id sq, es-interval wf2, es-info wf